T:Type, l1:T List, v:T, l2:T List. l1  l2  ||l1||<||l2|| & l2[||l1||] = v  l1 @ [v]  l2 

latex

Definitions	t  T, x:A. B(x), as @ bs, Prop, ||as||, tl(l), x:A. B(x), A & B, ij, P  Q, l[i], l1  l2, P  Q, P & Q, P  Q, False, A, AB, True, T, i  j < k, {i..j}, , {T}, SQType(T), hd(l), i<j, ij
Lemmas	cons one one, nat wf, member wf, select append back, squash wf, le wf, length append, append assoc, length wf1, select wf, non neg length, tl wf, append wf